perm filename TOUGH[W83,JMC] blob sn#701708 filedate 1983-03-14 generic text, type C, neo UTF8
COMMENT āŠ—   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.<<tough[w83,jmc]		Tough nuts for computer science, IFIP 83>>
C00016 ENDMK
CāŠ—;
.<<tough[w83,jmc]		Tough nuts for computer science, IFIP 83>>
.require "memo.pub[let,jmc]" source
.FONT B "zero30";
John McCarthy

	My discussion will focus on two topics: the present status of the
problems discussed in my "Problems in the Theory of Computation" given at
the 1965 World Computer Congress in New York.  The second topic concerns
features of natural language description of processes not yet offered in
programming languages.

	My 1965 paper begins

	%2"The prize to be won if we can
develop a reasonable mathematical theory of computation is the
elimination of debugging.  Instead, a programmer will prepare
a computer-checked proof that a program has the desired properties.

 .
 .
 .

	%2I believe that this goal can be achieved, but we are a long
way from it now.  The purpose of this paper is to list some subgoals.
In my opinion each of these problems is solvable, is theoretically
interesting, and contributes to the understanding required for
a practical theory"%1.

	In 1965 the only approach to proving programs correct was
the functional approach described in my two 1963 papers.  Floyd's
inductive assertion method, anticipated by Turing in connection
with a particular program in 1945, was not published till 1967.
Since that time there has been an explosion of effort in developing
program verification methods, but the above goals are still in the
future.

	Here is a summary of the problems listed in that paper.

	1. Develop a language for expressing facts about
programs that accepts proofs close to a programmer's informal reasoning.
There is some progress.

	2. Express properties of programs not known to terminate.
This is now well understood.

	3. Conventions for describing languages, data spaces, computers
and algorithms in such a form that the relations among them can
be explored.  There still isn't a satisfactory general system.

	Here were some specific problems.

	1. Extend first order logic to include partial predicates
and functions.  This has been done in various ways.  Notable are
(Scott, many papers), (Cartwright 1976) and (Cartwright and McCarthy 1979).

	2. Develop the state vector approach to the semantics of
programming languages.  Much has been done in this direction.

	3. Develop a theory of syntax directed computing.  Almost
nothing has been done except for informal proofs about specific
syntax directed algorithms.


.skip to column 1
New Problems:

	My 1965 paper was directed to a particular area of computer
science, and the present task is more general.  Here are some goals.

	1. An approximate quantitative theory allowing one to divide
the size of the abstract execution of an algorithm by the speed of
a computer to get the time required.  Consider, for example, suppose
one wanted to have a computer chess tournament where the computers
were handicapped according to speed, so that algorithms rather
than whole systems were competing.  This is an old question, but
it needs to be revived from time to time.

	2. Programming languages that allow more of the essential useful
features of natural language.  In my view the syntax of natural language
is not its main useful feature, and experience has shown that programming
languages that merely require English syntax be used to express the same
programs that could be written in Algol is not an advance.  COBOL's
utility, such as it is, is based on its semantic features and not on its
syntax.

	a. A key feature of natural language is the ability to
request a modified procedure without fully understanding the
original procedure.  For example, an airline official could tell
his programmers to have the reservation program ask for the nationality
of the passenger and avoid seating nationals of specified warring
countries next to each other.  In order to do this, the official
doesn't have to know how the existing program works.  However, the
programmer cannot tell the computer to do this without reading much
of the existing program.  As much as possible, we need to be able
to change programs without reading them.

	b. In natural language, we don't usually have to specify
data structures.  For example, the airline official originally
specifying a reservation system might say: The program should
accept reservations if the number of reservations is less than
the capacity of the flight, it should allow the passenger to
cancel a reservation, and it should answer when asked whether
a passenger has a reservation.  There is nothing in this specification
about a data structure for remembering reservations, and we can
imagine a compiler for a language that would decide on a data
structure only after the desired-input output behavior is specified.
The key fact is that a passenger has a reservation if he has
made one and not cancelled it.  A programming language that
allowed this to be said has to allow statements to refer to
the occurrence of past events rather than to the present status
of a data structure into which information has been stored.
The compiler itself should decide to use an array of length
equal to the number of seats on the flight.

	To see that this represents a decision by the compiler,
imagine that the official decided to modify the procedure so that
it could be answered whether as passenger had ever made a reservation.
Then the compiler would require a different data structure, since
it is no longer permissible to forget cancelled reservations.

	It is even more powerful to allow reference to the future.
"Baggage handlers shall be summoned to the airport one hour before
the airplane arrives".  A language permitting reference to the
future may contain contradictory programs which therefore couldn't
be compiled.  Most likely it will be undecidable in general whether
a futuristic program is compilable.  However, compilers will be
able to try and know whether or not they have succeeded.

	I have been trying to specify a programming language
called Elephant (it never forgets) that would allow such programs.

	c. Present programming languages for describing concurrent
processes require explicit attention to synchronization, fairness,
etc.  Natural language description of concurrent processes
rarely has to be explicit about such matters.

	d. The meta-problem is to identify other semantic features of natural
language description of procedures that aren't in present programming
languages.

	3. Common business communication language.  This is a problem
on the boundary of computer science, artificial intelligence, linguistics
and business.  The full utility of computers in business requires
that computers belonging to different organizations communicate
with one another - even computers whose owners have never heard of
each other.  For example, a Company A's computer might extract
the fact that company B's computer supplies widgets from a database,
then telephone Company B's computer and ask what price and delivery
is available on 300 Number 5 widgets, each with 8 megabytes of memory
and white sidewall tires.  Company B's computer might respond with
a price and a statement that they could be delivered starting in
six months at a rate of 20 per month provided the production capacity
wasn't pre-empted by a Government order.

	This relatively fancy example illustrates the fact that
standardizing such intercomputer business communication requires
formalization of an interesting subset of natural language semantics.
See (McCarthy 1982) for more of this.

References:

%3McCarthy, John (1965)%1: "Problems in the Theory of Computation", in Proc.
IFIP Congress 65, Spartan, Washington, D.C..

%3Cartwright, R.S. (1977)%1:
%2A Practical Formal Semantic Definition and Verification System
for Typed Lisp%1,
Ph.D. Thesis, Computer Science Department, Stanford University,
Stanford, California.

%3Cartwright, Robert and John McCarthy (1979)%1:
"Recursive Programs as Functions in a First Order Theory",
in %2Proceedings of the International Conference on Mathematical Studies of
Information Processing%1, Kyoto, Japan.
.<<aim 324, FIRST.NEW[W77,JMC]>>

%3McCarthy, John (1982)%1: "Common Business Communication Language", in
%2Textverarbeitung und B%B:%*urosysteme%1, Albert Endres and J%B:%*urgen Reetz, eds.
R. Oldenbourg Verlag, Munich and Vienna 1982.